T:Type, l:(T List), P:(T), x,y:T.
l_before(x; y; filter(P; l); T)  (((P(x)))  ((P(y)))  l_before(x; y; l; T)) 

latex

Definitions	P  Q, P  Q, P  Q, x. t(x), P  Q, prop{i:l}, t  T, x(s), x:A. B(x)
Lemmas	l all nil, l member wf, assert wf, l all wf, filter wf, sublist wf